Inference at * 1 1 2 1 
Iof proof for Lemma adjacent-append:



1. T : Type
2. x : T
3. y : T
4. L1 : T List
5. L2 : T List
6. i : {0..(||L1 @ L2|| - 1)}
7. x = (L1 @ L2)[i]
8. y = (L1 @ L2)[(i+1)]
9. i < ||L1||
10. (i < (||L1|| - 1))
  (0 < ||L1||) & (0 < ||L2||) & x = last(L1) & y = hd(L2) 

latex

 by ((((RWO "select_append_front" (-4)) 
CollapseTHENA (Auto'))) 
CollapseTHEN (((
CRWO "select_append_back" (-3)) 
CollapseTHENA (Auto')))) 

latex

C1: 

C1: 7. x = L1[i]
C1: 8. y = L2[((i+1) - ||L1||)]
C1: 9. i < ||L1||
C1: 10. (i < (||L1|| - 1))
C1:   (0 < ||L1||) & (0 < ||L2||) & x = last(L1) & y = hd(L2)
C.

Definitions	, P  Q, P  Q, #$n, l[i], t  T, x:A  B(x), Void, i  j < k, P & Q, False, P  Q, n - m, -n, n+m, A, a < b, {x:A| B(x)} , , type List, Type, {i..j}, ||as||, as @ bs, i  j , A  B, x:A. B(x), x:AB(x), s = t
Lemmas	select append front, iff wf, rev implies wf, select append back, le wf, append wf, non neg length, length append